Step of Proof: add_functionality_wrt_le
12,41
postcript
pdf
Inference at
*
1
I
of proof for Lemma
add
functionality
wrt
le
:
1.
i1
:
2.
i2
:
3.
j1
:
4.
j2
:
5.
i1
j1
6.
i2
j2
(
i1
+
i2
)
(
j1
+
j2
)
latex
by MoveToConcl 3
latex
1
:
1:
3.
j2
:
1:
4.
i2
j2
1:
j1
:
. (
i1
j1
)
((
i1
+
i2
)
(
j1
+
j2
))
.
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
P
Q
origin